(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 16))
(declare-fun a1 () (Array  (_ BitVec 1)  (_ BitVec 8)))
(declare-fun a2 () (Array  (_ BitVec 13)  (_ BitVec 8)))
(assert (let ((e3(_ bv1 3)))
(let ((e4(_ bv334 9)))
(let ((e5 ((_ zero_extend 0) v0)))
(let ((e6 (bvsrem e3 e3)))
(let ((e7 (bvand e4 ((_ sign_extend 6) e6))))
(let ((e8 (store a2 ((_ sign_extend 10) e3) ((_ extract 14 7) v0))))
(let ((e9 (store a2 ((_ extract 13 1) v0) ((_ extract 8 1) e7))))
(let ((e10 (select e9 ((_ zero_extend 4) e7))))
(let ((e11 (select a1 ((_ extract 2 2) e4))))
(let ((e12 (store e8 ((_ sign_extend 10) e6) ((_ sign_extend 5) e3))))
(let ((e13 (select e12 ((_ extract 15 3) v0))))
(let ((e14 (select e9 ((_ zero_extend 5) e10))))
(let ((e15 (bvxor e7 ((_ zero_extend 1) e14))))
(let ((e16 (bvand ((_ zero_extend 6) e3) e4)))
(let ((e17 (ite (bvslt e15 ((_ sign_extend 1) e13)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (= (_ bv1 1) ((_ extract 3 3) e5)) ((_ zero_extend 2) e17) e6)))
(let ((e19 (bvor v0 ((_ zero_extend 13) e6))))
(let ((e20 (bvadd ((_ sign_extend 13) e3) e5)))
(let ((e21 (bvsub v0 ((_ sign_extend 8) e14))))
(let ((e22 ((_ sign_extend 0) e11)))
(let ((e23 ((_ zero_extend 12) e17)))
(let ((e24 (ite (bvugt ((_ zero_extend 15) e17) e5) (_ bv1 1) (_ bv0 1))))
(let ((e25 (ite (distinct ((_ sign_extend 8) e10) e5) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvugt e4 ((_ zero_extend 8) e24))))
(let ((e27 (bvslt e4 e15)))
(let ((e28 (bvsgt e20 ((_ sign_extend 13) e3))))
(let ((e29 (bvsle e19 ((_ sign_extend 8) e14))))
(let ((e30 (bvugt e11 e13)))
(let ((e31 (bvule e19 e5)))
(let ((e32 (bvsle e6 ((_ sign_extend 2) e17))))
(let ((e33 (bvsle ((_ zero_extend 8) e25) e4)))
(let ((e34 (bvult e19 ((_ sign_extend 15) e24))))
(let ((e35 (distinct v0 ((_ sign_extend 8) e13))))
(let ((e36 (bvsgt ((_ sign_extend 8) e11) e5)))
(let ((e37 (bvule e6 e3)))
(let ((e38 (bvsle e21 ((_ zero_extend 8) e10))))
(let ((e39 (= ((_ sign_extend 7) e17) e11)))
(let ((e40 (distinct e20 ((_ sign_extend 13) e6))))
(let ((e41 (bvuge e21 ((_ sign_extend 15) e25))))
(let ((e42 (bvult ((_ sign_extend 8) e17) e16)))
(let ((e43 (bvslt ((_ zero_extend 13) e3) e20)))
(let ((e44 (bvslt e19 ((_ zero_extend 13) e6))))
(let ((e45 (bvuge ((_ sign_extend 7) e15) e20)))
(let ((e46 (distinct ((_ sign_extend 5) e6) e13)))
(let ((e47 (bvuge e22 e10)))
(let ((e48 (bvuge e18 e6)))
(let ((e49 (bvsge e10 e13)))
(let ((e50 (distinct v0 ((_ sign_extend 8) e14))))
(let ((e51 (= e18 ((_ zero_extend 2) e17))))
(let ((e52 (distinct e21 ((_ zero_extend 15) e25))))
(let ((e53 (distinct e10 ((_ zero_extend 7) e24))))
(let ((e54 (= e13 e11)))
(let ((e55 (bvugt ((_ zero_extend 3) e23) e21)))
(let ((e56 (bvslt e16 ((_ sign_extend 6) e18))))
(let ((e57 (bvule ((_ sign_extend 1) e11) e16)))
(let ((e58 (bvsgt e10 ((_ sign_extend 5) e6))))
(let ((e59 (bvule e20 ((_ sign_extend 15) e24))))
(let ((e60 (bvule e23 ((_ sign_extend 10) e3))))
(let ((e61 (= e7 ((_ sign_extend 1) e11))))
(let ((e62 (or e31 e36)))
(let ((e63 (ite e37 e48 e58)))
(let ((e64 (not e33)))
(let ((e65 (or e28 e38)))
(let ((e66 (= e43 e32)))
(let ((e67 (=> e65 e62)))
(let ((e68 (ite e27 e64 e50)))
(let ((e69 (=> e51 e59)))
(let ((e70 (not e35)))
(let ((e71 (or e67 e61)))
(let ((e72 (and e55 e71)))
(let ((e73 (not e57)))
(let ((e74 (ite e52 e46 e47)))
(let ((e75 (or e34 e26)))
(let ((e76 (xor e29 e44)))
(let ((e77 (= e30 e53)))
(let ((e78 (=> e75 e40)))
(let ((e79 (xor e54 e63)))
(let ((e80 (ite e77 e69 e70)))
(let ((e81 (=> e41 e49)))
(let ((e82 (= e68 e78)))
(let ((e83 (or e73 e60)))
(let ((e84 (ite e42 e39 e76)))
(let ((e85 (or e80 e81)))
(let ((e86 (or e83 e72)))
(let ((e87 (=> e74 e84)))
(let ((e88 (=> e45 e82)))
(let ((e89 (and e86 e87)))
(let ((e90 (=> e89 e79)))
(let ((e91 (not e88)))
(let ((e92 (and e85 e66)))
(let ((e93 (xor e56 e56)))
(let ((e94 (= e92 e90)))
(let ((e95 (ite e91 e94 e93)))
(let ((e96 (and e95 (not (= e3 (_ bv0 3))))))
(let ((e97 (and e96 (not (= e3 (bvnot (_ bv0 3)))))))
e97
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
